\begin{tabbing}
weak{-}precond{-}send{-}p(${\it es}$;$T$;$A$;$l$;${\it tg}$;$a$;${\it ds}$;$P$;$f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(($\forall$$x$:Id. vartype(source($l$);$x$) $\subseteq$r ${\it ds}$($x$)?Top)\+
\\[0ex]\& $\forall$$e$@source($l$). (kind($e$) = locl($a$)) $\Rightarrow$ (valtype($e$) $\subseteq$r $A$)
\\[0ex]\& ($\forall$$e$:E. (kind($e$) = rcv($l$,${\it tg}$)) $\Rightarrow$ (valtype($e$) $\subseteq$r $T$)))
\\[0ex]c$\wedge$ \=((\=$\forall$${\it e'}$:E.\+\+
\\[0ex](kind(${\it e'}$) = rcv($l$,${\it tg}$))
\\[0ex]$\Rightarrow$ \=((kind(sender(${\it e'}$)) = locl($a$))\+
\\[0ex]c$\wedge$ \=(($\uparrow$($P$((state when sender(${\it e'}$)))))\+
\\[0ex]\& val(${\it e'}$) = $f$((state when sender(${\it e'}$)),val(sender(${\it e'}$))))))
\-\-\-\\[0ex]\& \=$\forall$$e$@source($l$).\+
\\[0ex]$\exists$\=${\it e'}$:E\+
\\[0ex]($e$ c$\leq$ ${\it e'}$
\\[0ex]\& (\=((kind(${\it e'}$) = rcv($l$,${\it tg}$)) c$\wedge$ $e$ $\leq$loc sender(${\it e'}$) )\+
\\[0ex]$\vee$ ((loc(${\it e'}$) = source($l$)) c$\wedge$ ($\neg$($\forall$$t$:$\mathbb{Q}$. $\uparrow$($P$((state after ${\it e'}$)+$t$))))))))
\-\-\-\-\-
\end{tabbing}